#include <typeinfo>

#include "atom.h"
#include "bind.h"
#include "configuration.h"
#include "prover.h"
#include "predicates.h"
#include "system.h"
#include "trail.h"
#include "tree.h"
#include "tuple.h"

bool Binder::bindDoNotRollback (pNode p1, pNode p2, Trail &trail) {
  Node &f1 = *p1.final (), &f2 = *p2.final ();
  if(&f1 == &f2)
    return true;

  if(typeid(f1) == typeid(Reference))
    f1.bound (f2, trail);
  else if(typeid(f2) == typeid(Reference))
    f2.bound (f1, trail);
  else if(typeid(f1) != typeid(f2))
    return false;

  else if(typeid(f1) == typeid(Atom))
    return false; // Atoms are all pooled, so pointer comparison should work
  else if(typeid(f1) == typeid(String))
    return static_cast<Atom&> (f1).name == static_cast<Atom&> (f2).name;
  else if(typeid(f1) == typeid(Number))
    return static_cast<Number&> (f1).value == static_cast<Number&> (f2).value;
  else if(typeid(f1) == typeid(Tuple)) {
    Tuple &t1 = static_cast<Tuple&> (f1), &t2 = static_cast<Tuple&> (f2);
    unsigned int size = t1.nodes.size ();
    if(size != t2.nodes.size ())
      return false;

    for(unsigned int i = 0; i < size; i++)
      if(!bindDoNotRollback (t1.nodes[i], t2.nodes[i], trail))
        return false;
  } else if(typeid(f1) == typeid(Tree)) {
    Tree & type1 = static_cast<Tree&> (f1), &type2 = static_cast<Tree&> (f2);

    if(strncmp (type1.ops, type2.ops, 2) != 0 || !bindDoNotRollback (
        type1.left, type2.left, trail) || !bindDoNotRollback (type1.right,
        type2.right, trail))
      return false;
  } else
    return false;

  return true;
}

// Turns a variable as a different one in a smaller scope
class local : public OnceBindTupleProver {
predicateName("local")
  local () :
    prover (0) {
  }
  ~local () {
    if(prover)
      delete prover;
  }

  bool proveOnce () {
    int n = tuple->nodes.size () - 2;
    Reference *refs[n];

    // Must be variables or things would break
    for(int i = 0; i < n; i++) {
      Reference &varRef =
          static_cast<Reference&> (*tuple->nodes[i + 1].final ());
      refs[i] = &varRef;
      varRef.target = new Reference;
    }

    prover = Prover::create (*tuple->nodes[n + 1], *system);
    bool ret = prover->prove ();

    for(int i = 0; i < n; i++)
      refs[i]->target = 0;

    return ret;
  }

  Prover *prover;
};

ProverFactoryRegistrar<local, Tuple::ID> localRegistrar;

class same : public OnceBindTupleProver {
predicateName("same")

  bool proveOnce () {
    return tuple->nodes[1].final () == tuple->nodes[2].final ();
  }
};

ProverFactoryRegistrar<same, Tuple::ID, 3> sameRegistrar;

// Separate trail for a block of predicates
class trail : public OnceProver {
predicateName("trail")
  trail () :
    prover (0) {
  }
  ~trail () {
    if(prover)
      delete prover;
  }

  bool proveOnce () {
    System newSystem (system->rules, system->globals, newTrail);
    prover = Prover::create (*tuple->nodes[1], newSystem);

    if(prover->prove ())
      return true;
    else {
      newTrail.rollback ();
      return false;
    }
  }

  Prover *prover;
  Tuple *tuple;
  System *system;
  Trail newTrail;
  void set (Tuple &t, System &s) {
    tuple = &t;
    system = &s;
  }
};

ProverFactoryRegistrar<trail, Tuple::ID, 2> trailRegistrar;
